<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue3322</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Background">% Nisse, 2018-10-26
% Testing that record field are already highlighted by scope checker.

\documentclass{article}

\usepackage{agda}

% This redefinition of AgdaField,
% in combination with the math-only command \bot,
% will fail the LaTeX build if no highlighting
% of fields has been performed.

\renewcommand{\AgdaField}[1]{\ensuremath{#1}}

\usepackage{amsmath}
\usepackage{newunicodechar}
\newunicodechar{₁}{\ensuremath{{}_{\text{1}}}}
\newunicodechar{₂}{\ensuremath{{}_{\text{2}}}}
\newunicodechar{⊥}{\bot}

\pagestyle{empty}

\begin{document}

</a><a id="553" class="Markup">\begin{code}</a>
<a id="566" class="Keyword">record</a> <a id="R"></a><a id="573" href="Issue3322.html#573" class="Record">R</a> <a id="575" class="Symbol">:</a> <a id="577" class="PrimitiveType">Set₂</a> <a id="582" class="Keyword">where</a>
  <a id="590" class="Keyword">field</a>
    <a id="R.⊥"></a><a id="600" href="Issue3322.html#600" class="Field">⊥</a> <a id="602" class="Symbol">:</a> <a id="604" class="PrimitiveType">Set₁</a>

<a id="r"></a><a id="610" href="Issue3322.html#610" class="Function">r</a> <a id="612" class="Symbol">:</a> <a id="614" href="Issue3322.html#573" class="Record">R</a>

<a id="617" href="Issue3322.html#610" class="Function">r</a> <a id="619" class="Symbol">=</a> <a id="621" class="Keyword">record</a> <a id="628" class="Symbol">{</a> <a id="630" href="Issue3322.html#600" class="Field">⊥</a> <a id="632" class="Symbol">=</a> <a id="634" class="PrimitiveType">Set</a> <a id="638" class="Symbol">}</a>
<a id="640" class="Markup">\end{code}</a><a id="650" class="Background">

\end{document}
</a></pre></body></html>